\begin{tabbing}
SESAxioms\=\{i:l\}\+
\\[0ex]($E$; $T$; ${\it pred?}$; ${\it info}$; ${\it when}$; ${\it after}$; ${\it time}$)
\-\\[0ex]$\,\equiv$$_{\mbox{\scriptsize def}}$$\;\;$\=(\=$\forall$$e$:$E$, $l$:IdLnk.\+\+
\\[0ex]$\exists$\=${\it e'}$:$E$\+
\\[0ex]($\forall$${\it e''}$:$E$.
\\[0ex]($\uparrow$rcv?(${\it info}$;${\it e''}$))
\\[0ex]$\Rightarrow$ (sender(${\it info}$;${\it e''}$) = $e$ $\in$ $E$)
\\[0ex]$\Rightarrow$ (link(${\it info}$;${\it e''}$) = $l$ $\in$ IdLnk)
\\[0ex]$\Rightarrow$ \=(((${\it e''}$ = ${\it e'}$ $\in$ $E$) $\vee$ cless($E$;${\it pred?}$;${\it info}$;${\it e''}$;${\it e'}$))\+
\\[0ex]\& loc(${\it info}$;${\it e'}$) = destination($l$) $\in$ Id)))
\-\-\-\\[0ex]\& (\=((\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+\+
\\[0ex](loc(${\it info}$;$e$) = loc(${\it info}$;${\it e'}$) $\in$ Id)
\\[0ex]$\Rightarrow$ (${\it pred?}$($e$) = ${\it pred?}$(${\it e'}$) $\in$ ($E$ + Unit))
\\[0ex]$\Rightarrow$ ($e$ = ${\it e'}$ $\in$ $E$))
\-\\[0ex]\& strongwellfounded($E$; $e$,${\it e'}$.pred!($E$;${\it pred?}$;${\it info}$;$e$;${\it e'}$))
\\[0ex]\& ($\forall$$e$:$E$. ($\neg$($\uparrow$first(${\it pred?}$;$e$))) $\Rightarrow$ (loc(${\it info}$;pred(${\it pred?}$;$e$)) = loc(${\it info}$;$e$) $\in$ Id))
\\[0ex]\& (\=$\forall$$e$:$E$.\+
\\[0ex]($\uparrow$rcv?(${\it info}$;$e$)) $\Rightarrow$ (loc(${\it info}$;sender(${\it info}$;$e$)) = source(link(${\it info}$;$e$)) $\in$ Id))
\-\\[0ex]\& (\=$\forall$$e$:$E$, ${\it e'}$:$E$.\+
\\[0ex]($\uparrow$rcv?(${\it info}$;$e$))
\\[0ex]$\Rightarrow$ ($\uparrow$rcv?(${\it info}$;${\it e'}$))
\\[0ex]$\Rightarrow$ (link(${\it info}$;$e$) = link(${\it info}$;${\it e'}$) $\in$ IdLnk)
\\[0ex]$\Rightarrow$ cless($E$;${\it pred?}$;${\it info}$;sender(${\it info}$;$e$);sender(${\it info}$;${\it e'}$))
\\[0ex]$\Rightarrow$ cless($E$;${\it pred?}$;${\it info}$;$e$;${\it e'}$)))
\-\\[0ex]c$\wedge$ \=($\forall$$e$:$E$.\+
\\[0ex]($\neg$($\uparrow$first(${\it pred?}$;$e$)))
\\[0ex]$\Rightarrow$ \=($\forall$$x$:Id, $t$:$\mathbb{Q}$.\+
\\[0ex]${\it when}$($x$,$e$,$t$)
\\[0ex]=
\\[0ex]${\it after}$($x$,pred(${\it pred?}$;$e$),$t$ + ((${\it time}$($e$)) {-} (${\it time}$(pred(${\it pred?}$;$e$)))))
\\[0ex]$\in$ $T$(loc(${\it info}$;$e$),$x$))))
\-\-\-\-
\end{tabbing}